package org.xtext.runtime.util;

import org.xtext.runtime.formula.ACREASTRAEvent;
import org.xtext.runtime.formula.CartagoPropertyEvent;
import org.xtext.runtime.formula.Event;
import org.xtext.runtime.formula.Goal;
import org.xtext.runtime.formula.MentalEvent;
import org.xtext.runtime.formula.MessageEvent;
import org.xtext.runtime.formula.Predicate;
import org.xtext.runtime.term.ITerm;
import org.xtext.runtime.term.Variable;
import org.xtext.runtime.type.TypeException;

/**
 * This class performs unification of various logical formulae: {@link Predicate},
 * {@link Goal}, and {@link MentalEvent}.
 * 
 * The core work in this class is done in the private method.
 *  
 * @author rem
 *
 */
public class Unifier {
	/**
	 * Generate variable bindings for two predicates or return null if there is no binding...
	 * 
	 * @param source first predicate
	 * @param target second predicate
	 * @return a {@link Bindings} object or null
	 */
	public static Bindings unify(Predicate source, Predicate target) {
		if  (source.identifier().equals(target.identifier()) && source.size() == target.size()) {
			return unify(source.terms(), target.terms());
		}
		return null;
	}

	/**
	 * Generate variable bindings for two achievement goals or return null if there is no binding...
	 * 
	 * @param source first goal
	 * @param target second goal
	 * @return a {@link Bindings} object or null
	 */
	public static Bindings unify(Goal source, Goal target) {
		return unify(source.formula(), target.formula());
	}

	/**
	 * Generate variable bindings for two events or return null if there is no binding...
	 * 
	 * @param source first event
	 * @param target second event
	 * @return a {@link Bindings} object or null
	 */
	public static Bindings unify(MentalEvent source, MentalEvent target) {
		if  (source.type() == target.type()) {
			if (source.formula() instanceof Predicate && target.formula() instanceof Predicate) {
				return unify((Predicate) source.formula(), (Predicate) target.formula());
			} else if (source.formula() instanceof Goal && target.formula() instanceof Goal) {
				return unify((Goal) source.formula(), (Goal) target.formula());
			}
		}
		return null;
	}

	public static Bindings unify(MessageEvent source, MessageEvent target) {
		try {
			if (!source.performative().equals(target.performative())) return null;
			Bindings bindings = unify(new ITerm[] {source.sender()}, new ITerm[] {target.sender()});
			if (bindings != null) {
				Bindings temp = unify(source.content(), target.content());
				if (temp != null) {
					bindings.addAll(temp);
					return bindings;
				}
			}
		} catch (BindingException e) {
			return null;
		} catch (TypeException e) {
			return null;
		}
		return null;
	}

	public static Bindings unify(CartagoPropertyEvent source, CartagoPropertyEvent target) {
		try {
			if (!source.type().equals(target.type())) return null;
			Bindings bindings = unify(new ITerm[] {source.id()}, new ITerm[] {target.id()});
			if (bindings != null) {
				Bindings temp = unify(source.content(), target.content());
				if (temp != null) {
					bindings.addAll(temp);
					return bindings;
				}
			}
		} catch (BindingException e) {
			return null;
		} catch (TypeException e) {
			return null;
		}
		return null;
	}

	public static Bindings unify(ACREASTRAEvent source, ACREASTRAEvent target) {
		if (!source.type().equals(target.type())) return null;
		if (source.type().equals(ACREASTRAEvent.ADVANCED)) {
			return unify(new ITerm[] {source.conversationId(), source.state(), source.length()}, new ITerm[] {target.conversationId(), target.state(), target.length()});
		} /*else if (source.type().equals(ACREASTRAEvent.UNMATCHED) || source.type().equals(ACREASTRAEvent.AMBIGUOUS)) {
			return null;
		} */else if (source.type().equals( ACREASTRAEvent.MESSAGE)) {
		   if (!source.performative().equals(  target.performative())) {
		      return null;
		   }
		   Bindings bindings = unify(new ITerm[] {source.conversationId()}, new ITerm[] {target.conversationId()});
         if (bindings != null) {
            Bindings temp = unify(source.content(), target.content());
            if (temp != null) {
               try {
                  bindings.addAll(temp);
                  return bindings;
               }
               catch ( BindingException e ) {
                  // TODO Auto-generated catch block
                  e.printStackTrace();
                  return null;
               }
               catch ( TypeException e ) {
                  // TODO Auto-generated catch block
                  e.printStackTrace();
                  return null;
               }
            }
         }
         return null;
		} else {
			return unify(new ITerm[] {source.conversationId()}, new ITerm[] {target.conversationId()});
		}
	}

	private static Bindings unify(ITerm[] source, ITerm[] target) {
		Bindings bindings = new Bindings();
		for (int i=0; i < source.length; i++) {
			ITerm sourceTerm = source[i];
			ITerm targetTerm = target[i];

			// Check that the types match
			if (!sourceTerm.type().matches(targetTerm.type())) {
				System.out.println("[Unifier] checking: " + sourceTerm + " / " + targetTerm);
				System.out.println("[Unifier] type mismatch..." + sourceTerm.type() + " / "+ targetTerm.type());
				return null;
			}
			
			// Do the actual unification of the terms...
			if (Variable.class.isInstance(sourceTerm)) {
				Variable var = (Variable) sourceTerm;
				if (var.isFree()) {
					try {
						var.assign(targetTerm);
						bindings.addVariable(var);
					} catch (TypeException e) {
						return null;
					} catch (BindingException e) {
						return null;
					}
				} else if (Variable.class.isInstance(targetTerm)) {
					Variable var2 = (Variable) targetTerm;
					if (var2.isFree()) {
						try {
							var2.assign(var.value());
							bindings.addVariable(var2);
						} catch (TypeException e) {
							return null;
						} catch (BindingException e) {
							return null;
						}
					}					
				} else {
					if (!var.value().equals(targetTerm)) {
						return null;
					}
				}
			} else if (Variable.class.isInstance(targetTerm)) {
				Variable var = (Variable) targetTerm;
				if (var.isFree()) {
					try {
						var.assign(sourceTerm);
						bindings.addVariable(var);
					} catch (TypeException e) {
						return null;
					} catch (BindingException e) {
						return null;
					}
				} else {
					if (!var.value().equals(sourceTerm)) {
						return null;
					}
				}
			} else if (!sourceTerm.equals(targetTerm)) {
				return null;
			}
			
		}
		return bindings;
	}

	public static Bindings unify(Event event, Event event2) {
		if (event instanceof MentalEvent && event2 instanceof MentalEvent) {
			return unify((MentalEvent) event, (MentalEvent) event2);
		} else if (event instanceof MessageEvent && event2 instanceof MessageEvent) {
			return unify((MessageEvent) event, (MessageEvent) event2);
		} else if (event instanceof CartagoPropertyEvent && event2 instanceof CartagoPropertyEvent) {
			return unify((CartagoPropertyEvent) event, (CartagoPropertyEvent) event2);
		} else if (event instanceof ACREASTRAEvent && event2 instanceof ACREASTRAEvent) {
			return unify((ACREASTRAEvent) event, (ACREASTRAEvent) event2);
		}
		return null;
	}
}
